Logic to IP Formulas: Computational Tools and Applications

Harry G. Kwatny
Edoe Mensah

Department of Mechanical Engineering & Mechanics
Drexel University
Philadelphia PA 19104

1. Introduction

Often, the role of logic in mathematical programming goes unrecognized. Three decades ago,  it was shown that  posing logical inference as a mathematical programming problem opens up the possibility of transfering the computational techniques of mathematical programming to the symbolic world of logic.
The classical approach of integer programming modeling based on a quantitative paradigm, presents some limitations in introducing qualitative features of modern day complex decision making problems. In addition to the inability of a non-specialist to interprete purely quantitative results, and its limitations for specification of  real world problems, researchers have developed and continue to develop new algorithms that will enable the modeling of qualitative information often encountered in complex decision support procedures. 
The most significant contribution came from Robert Jeroslow and Paul Williams in their works on the connections between logic and mathematical programming [4]. Granot and Hammer in 1970, Hammer and Peled in 1972 had exploited the analogy between Boolean algebra and 0-1 programming. And later F. Glover in 1975 represents coupling between logical and continuous variables as linear inequalities on binary and continuous variable. Based on these preexisting logic ideas Morari and Bemporad recently devised the Mixed logical Dynamical systems framework for hybrid systems [9]
Qiang Li, Yike Guo and Tetsuo Ida had proposed a modeling language for IP based on the propositional logic and a systematic algorithm for transforming logic formulas into IP formulas using mathematica. Our goal is to improved the proposed  modeling language and use it for modeling hybrid systems.

2. Propositional Logic

Atomic formula: are proposition without logical connectives.
It will state either  an object is a member of a set, or that it is equal to another set.
Valid atomic proposition: 
Tomorrow is tuesday: true if today is monday False if not
2+2=5:False

The syntax is the set of rules defining how atomic formula may be combined to well-formed formulas.
Every atomic formula is a well-formed formula
An alphabet of symbols:(∧,∨,¬,⇒,⇔(,), a,b,..z, a1,b1,..z1,....)
Rules:
Negation: ¬p
Conjunction: p∧q
Disjunction:  p∨q
Implication:  p⇒q
Equivalence:p⇔q
If p and q are well-formed formulas then, so are:(¬p), (¬q), ( p∧q), ( p∨q), (p⇒q), (p⇔q)

It characterizes the meaning of the logical proposition with respect to a specified frame. The frame is a set of states through which a system might evolve ( ie hybrid automaton).

A clause is a logical formula with literals in disjunctive form.Ex: x1 ∨ ¬x2∨x3
A formula is in clausal form (CF) or Conjunctive Normal From (CNF) is it a conjunction of clauses. 
Ex:(x1 ∨ ¬x2∨x3)∧(x1 ∨ ¬x2∨¬x3)
The dual of the conjunctive normal form is the disjunctive normal form. it is the disjunction of conjounctive literals: 
Ex: (x1∧ ¬x2)∨(x2∧¬x3)
 A boolean function f(x) is defined by the list of assignments that make it false.This function can be express in CNF by writing a formula that rules out all such assignment.
 Let write a boolean function which is  false when (x1,x2)=(1,1) or (0,0) and true otherwise:(¬x1∨¬x2)∧(x1∨x2) 
 Constraint satisfaction: (satisfiability)
 Any constraint whose variables are two-valued can be interpreted as defining a boolean function f(x) that is false when x is violate the constraint.
 Ex : the 0-1 inequality 3x1+2x2+x3≥4 defines a set a boolean function f(x) that is false when x1=0 or (x2,x3)=(0,0)  and true otherwise.
 The inequality is therefore equivalent to the clause set: { x1 , x2∨x3}
 A dual principle operates for DNF formulas. A DNF equivalent of a boolean function f(x1,x2) defined by (¬x1∨¬x2)∧(x1∨x2), which is true for (x1,x2)=(0,1) and (x1,x2)=(1,0) , can be written as the DNF  formula.  (¬x1∧ x2)∨(x1∧¬x2)
 Neither a CNF nor DNF representation of a boolean function is unique .
 For example the following  CNF formulas represent the same boolean function: (x1∨x2)∧(¬x1∨x2) , (x1∨x2)∧(¬x1∨x2)∧(x2∨x3).
 In general compound proposition will have many different representation. In order to give comparable representations it is convenient to use one of the two common standard representations. CNF, DNF.
 Note: all unsatisfiable CNF formulas represent the same function, namely the constant function f(x)=0 and the DNF formulas represent f(x)=1

IP Formulas:
To each propositional variable p, we can associate a decision variable  p , a variable that can assume only two integer values {1,0}. 
(Subscript[δ, p]) = 1 means p=True
(Subscript[δ, p])= 0 means p=False

IP formulas are Integer programming
inequality constraints involving decision variables.
Or:        p ∨ q  ⟷ (Subscript[δ, p]) + (Subscript[δ, q])  ≥1
And:       p ∧ q  ⟷ (Subscript[δ, p]) ≥1,  (Subscript[δ, q])  ≥1
If then:    p ⇒q ⟷ ¬p ∨ q  ⟷1- (Subscript[δ, p]) + (Subscript[δ, q])≥1⟷  (Subscript[δ, q]) ≥ (Subscript[δ, p])
IFF:       p ⇔ q ⟷ (p ⇒ q) ∧ (q  ⇒ p)⟷ (Subscript[δ, q])  ≥ (Subscript[δ, p]) , (Subscript[δ, p])  ≥ (Subscript[δ, q])
XOr:      p ⊕ q ⟷ (p ∨ q )∧(¬ p∨¬ q ) ⟷ (Subscript[δ, p]) + (Subscript[δ, q])  ≥1, (Subscript[δ, p])+(Subscript[δ, q])≤1

3.  IP Functions

Function  ΓFormQ[x]  checks whether an expression is  Γ-form .

ΓFormQ[Γ[_, _]]  :=  True;
ΓFormQ[_]  :=  False;

Function VarQ[x] checks whether x is a propositional variable or an integer variable.

\(\(\(\ \)\(\(VarQ[x_Symbol] /; x =!= True\ \  ∧ x =!= False\  := 
        True;\)\ 

    \ \(VarQ[_] := False;\)\)\)\)

Function NegPVarQ[x] checks whether x is a negated propositional variable.

NegPVarQ[¬ x_Symbol] /; x =!= True   ∧ x =!= False :=  
        True;
NegPVarQ[_] := False;

Function PLiteralQ[p] checks whether p is a propositional variable or a negated  propositional variable

PLiteralQ[p_] := VarQ[p] ∨ NegPVarQ[p];
NotPLiteralQ[p_] := ¬ PLiteralQ[p]

Function BoundedQ[x] checks whether a variable x is properly bounded.

BoundedQ[m_Integer ≤ x_?VarQ ≤ n_Integer] := 
        True;
BoundedQ[m_Real ≤ x_?VarQ ≤ n_Integer] := 
        True;
BoundedQ[m_Integer ≤ x_?VarQ ≤ n_Real] := 
        True;
BoundedQ[m_Real ≤ x_?VarQ ≤ n_Real] := 
        True;
BoundedQ[m_Integer < x_?VarQ < n_Integer] := True;
BoundedQ[m_Real < x_?VarQ < n_Integer] := True;
BoundedQ[m_Integer < x_?VarQ < n_Real] := True;
BoundedQ[m_Real < x_?VarQ < n_Real] := True;
BoundedQ[_] :=  False;

Function ConstraintQ[c] checks whether an expression c  is a  constraint . Note that we use ==  to  denote the equality of symbol of \(TraditionalForm\`\(L\^+\)\).

\(\(\(\(ConstraintQ[
          x_ ≥ y_ | x_ > y_ | x_ ≤ y_\  | \ 
            x_ < y_\ \  | \ x_ == y_\ ] := \ True;\)

    \(ConstraintQ[_]\  := \ False;\)\)\(\ \)\)\)

Function  PredOrder[x,y] defines a predicate order in a Γ-formula.

PredOrder[x_?VarQ, r_[_, _]]  :=  True;
PredOrder[Not[_], r_[_, _]]  :=  True;
PredOrder[x_, y_]  := False

Function PLiteral2IPvar[e] translates a propositional variable e= p and a formula e=¬p into IP-formulas.

\(\(\(\(PLiteral2IPvar[x_?VarQ] := 
        Bounds[[\(Position[Bounds, 
              x]\)[[1, 1]], 
          2]]\ ;\)

    \(PLiteral2IPvar[¬ x_?VarQ] := 
        1 - Bounds[[\(Position[Bounds, 
                x]\)[[1, 1]], 
            2]]\ ;\)\)\(\ \)\)\)

Function Raux[x,y,z] is an auxiliary function of RuleR[x].

\(\(Raux[{x___?PLiteralQ, y___\ ?NotPLiteralQ}, m_, n_]\ \  := 
        Module[{newvarlist = Map[Unique["d"] &, {y}]}, 
          Bounds = 
            Bounds ⋃ 
              Map[0 ≤ # ≤ 1 &, 
                newvarlist]; 
		Prepend[
            Map[RuleR, 
              MapThread[
                Function[{d, a}, 
                  d > 0\  \[Implies] a], {newvarlist, {y}}]], \((Apply[Plus, 
                  newvarlist ⋃ 
                    Map[PLiteral2IPvar, {x}]] ≥ 
                m\ \ n)\)]];\)\)

Function RuleE[x] defines rule E.

RuleE1[x_] := 
        x //. {p_ ⇒ q_ -> ¬ p ∨ q };
RuleE2[x_]  := 
        x //. {p_ \[Implies] q_ -> ¬ p ∨ q, 
            p_⊕q_ -> (¬ q ∨ ¬ p) ∧ (p ∨ q), 
            p_ ⇔ 
                q_ -> ( 
                  p \[Implies] q) ∧ (q \[Implies] 
                    p)};
RuleE3[x_]  :=  
        x //. {p_⊕q_ -> (¬ q ∨ ¬ p) ∧ (p ∨ q)};
\(\(RuleE4[x_]\  := \ 
        x //. {p3_ ⇔ \((p1_⊕p2_)\) -> \((p2 ∨ ¬ p1 ∨ p3)\) ∧ \((p1 ∨ ¬ p2 ∨ 
                    p3)\) ∧ \((¬ p3 ∨ ¬ p1 ∨ ¬ p2)\) ∧ \((¬ p3 ∨ p1 ∨ 
                    p2)\), 
			\ p1_⊕p2_ ⇒ 
                p3_ -> \((p2 ∨ ¬ p1 ∨ 
                    p3)\) ∧ \((p1 ∨ ¬ p2 ∨ 
                    p3)\), 
			\ p3_ ⇒ 
                p1_⊕p2_ -> \((¬ p3 ∨ ¬ p1 ∨ ¬ p2)\) ∧ \((¬ p3 ∨ p1 ∨ 
                    p2)\), \ \ \ \ \ p_⊕q_ -> \((¬ q ∨ ¬ p)\) ∧ \((p ∨ q)\)};\)\)

Function  R[x] defines rule for Conjunctive Normal Form.

R1[x_]  :=  
        x //. {p_⊕q_ -> (¬ p ∨ ¬ q) ∧ (p ∨ q)};
R2[x_] := 
        x //. {A_ ⇒ B_ -> (¬ A ∨ B), 
            A_ ⇔ 
                B_ -> (¬ A ∨ 
                    B) ∧ (A ∨ ¬ B), (A_ ∨ ¬ A_) -> True, (¬ A_ ∨ A_) -> True};
R3[x_] := 
        x //. {¬ (A_ ∧ 
                    B_) -> (¬ A ∨ ¬ B), ¬ (A_ ∨ B_) -> (¬ A ∧ ¬ B)};
R4[x_] := 
        x //. {(A_ ∧ B_) ∨ 
                C_ -> (A ∨ C) ∧ (B ∨ C), 
            C_ ∨ (A_ ∧ B_) -> (C ∨ 
                    A) ∧ (C ∨ B)};
R5[x_] := 
        x //. {(A_ ∨ ¬ A_) -> 
              True, (¬ A_ ∨ A_) -> True};
R6[x_] := 
        x //. {(A_ ∨ A_) -> A};
CNF[Predicate_ ∧ x_] := 
      Predicate ∧ 
        CNF[R2[R1[RuleE1[RuleE2[x]]]]]
CNF[
        f_] := Not[
            LogicalExpand[Not[R2[R1[f]]]]] //. {Not[a_Or] :> 
              And @@ (Not /@ List @@ a), 
            Not[a_And] :> Or @@ (Not /@ List @@ a)} //. 
        A_ ⇒ B_ -> ¬ A ∨ 
            B

Function  E[x] defines rule for Disjunctive Normal Form.

E1[x_]  :=  
        x //. {p_⊕q_ -> (¬ p ∨ ¬ q) ∧ (p ∨ q)};
E2[x_] := 
        x //. {(A_ ⇒ B_) -> (¬ A ∨ 
                  B), ((A_) ⇒ 
                  B_) -> (¬ A ∨ 
                  B), ((A_) ⇒ 
                  B_) -> ¬ A ∨ B, 
            A_ ⇒ B_ -> ¬ A ∨ B, 
            A_ ⇔ 
                B_ -> (¬ A ∨ 
                    B) ∧ (A ∨ ¬ B)};
E3[x_] := 
      x //. {¬ (A_ ∧ 
                  B_) -> (¬ A ∨ ¬ B), ¬ (A_ ∨ B_) -> (¬ A ∧ ¬ B)}
E4[x_] := 
        x //. {(A_ ∨ B_) ∧ 
                C_ -> (A ∧ C) ∨ (B ∧ C), 
            C_ ∧ (A_ ∨ B_) -> (C ∧ 
                    A) ∨ (C ∧ 
                    B)};
E5[x_] := 
        x //. {(A_ ∨ ¬ A_) -> 
              True, (¬ A_ ∨ A_) -> 
              True};
E6[x_] := x //. {(A_ ∨ A_) -> A};
DNF[spec_] := Composition[E6, E5, E4, E3, E2, E1][spec]

Function  RuleT[x] defines rule T.

Clear[RuleT]

RuleT[x1_ ∨ x2_] := Γ[
          1, {RuleT[x1], RuleT[x2]}];
\(\(RuleT[x1_ ∧ x2_] := Γ[
          2, {RuleT[x1], RuleT[x2]}];\)
 (*
RuleT[
          x1_ ∧ x2_ ∧ x3_] := Γ[
          3, {RuleT[x1], RuleT[x2], RuleT[x3]}]; 
      RuleT[x1_ ∧ x2_ ∧ x3_ ∧ x4_] := Γ[
          4, {RuleT[x1], RuleT[x2], RuleT[x3], 
            RuleT[x4]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_] := Γ[
          5, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], 
            RuleT[x5]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_ ∧ 
            x6_] := Γ[
          6, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], RuleT[x5], 
            RuleT[x6]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_ ∧ x6_ ∧ 
            x7_] := Γ[
          7, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], RuleT[x5], 
            RuleT[x6], RuleT[x7]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_ ∧ x6_ ∧ 
            x7_ ∧ x8_] := Γ[
          8, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], RuleT[x5], 
            RuleT[x6], RuleT[x7], RuleT[x8]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_ ∧ x6_ ∧ 
            x7_ ∧ x8_ ∧ x9_] := Γ[
          9, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], RuleT[x5], 
            RuleT[x6], RuleT[x7], RuleT[x8], 
            RuleT[x9]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_ ∧ x6_ ∧ 
            x7_ ∧ x8_ ∧ x9_ ∧ x10_] := Γ[
          10, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], RuleT[x5], 
            RuleT[x6], RuleT[x7], RuleT[x8], RuleT[x9], 
            RuleT[x10]}]; 
RuleT[
          x1_ ∧ x2_ ∧ x3_ ∧ x4_ ∧ x5_ ∧ x6_ ∧ 
            x7_ ∧ x8_ ∧ x9_ ∧ x10_ ∧ 
            x11_] := Γ[
          11, {RuleT[x1], RuleT[x2], RuleT[x3], RuleT[x4], RuleT[x5], 
            RuleT[x6], RuleT[x7], RuleT[x8], RuleT[x9], RuleT[x10], 
            RuleT[x11]}];\ 
*) \)
RuleT[¬ x_] := ¬ RuleT[x] ;
RuleT[
          x_ ≠ y_] := ¬ RuleT[
            x == y];
RuleT[atleast[m_, S_]] := Γ[m, 
          Map[RuleT, S]];
RuleT[atmost[m_, S_]] := Γ[Length[S] - m, 
          Map[RuleT, Map[Not, S]]];
RuleT[none[S_]] := Γ[Length[S], 
          Map[RuleT, Map[Not, S]]];
RuleT[x_?VarQ] := PVarDecl[x];
RuleT[x_?ConstraintQ] := IPVarDecl[x];
RuleT[True] := Throw[{True, Bounds}];
RuleT[False] := 
        Throw["Wrong specification"];
RuleT[exactly[m_, S_]] := Γ[
          2, {RuleT[atleast[m, S]], RuleT[atmost[m, S]]}];

Function RuleN [x] defines rule N.

RuleN[Γ[m_, S_]] := Γ[m, 
          Map[RuleN, S]];
RuleN[¬ Γ[m_, S_]] := Γ[
          Length[S] - m + 1, Map[RuleN, Map[Not, S]]];
RuleN[¬ (x1_ == x2_)] := Γ[
          1, {x1 > x2, x1 < x2}];
RuleN[x_] := x;

Function  RuleF[x] defines rule  F.

RuleF[x_] := x  //. {RF1, RF2}
RF1 =  Γ [
            1, {x1___, Γ[1, {x2___}], 
              x3___}]  :>  Γ[1, {x1, x2, x3}];
RF2  =  Γ[
              m_, {x1___, Γ[n_, S_], x2___}] /; 
            m == Length[{x1, x2}] + 1 ∧ 
              n == Length[S]  :>   Γ[n + m - 1, 
            S ⋃ {x1, x2}];

Function  RuleR[x] defines rule R.

RuleR[r_[x1_, x2_]] := r[x1, x2];
RuleR[p_?PLiteralQ] := 
        PLiteral2IPvar[p] ⩾ 1;
RuleR[Γ[m_, S_]] /; m == Length[S] := 
        Map[RuleR, S];
RuleR[Γ[m_,  S_]]  /; m < Length[S] :=  
        Raux[Sort[S, PredOrder], m, 1];
RuleR[d_ > 0 \[Implies] Γ[m_, S_]] /; m == Length[S] := 
        Map[RuleR, Map[(d > 0 \[Implies] #) &, S]];
RuleR[d_ > 0 \[Implies] Γ[m_, S_]] /; m < Length[S] := 
        Raux[Sort[S, PredOrder], m, d];
RuleR[d_ > 0 \[Implies] p_?PLiteralQ] := 
        PLiteral2IPvar[p] ⩾ d;
RuleR[d_ > 0 \[Implies] x1_ ⩾ x2_] :=  
        Module[{L}, (Subscript[((x1 - x2  ⩾  L (1 - d ))), L])];
RuleR[d_ > 0 \[Implies] x1_ > x2_] := 
      Module[{L}, (Subscript[((x1 - x2  >  (L - 1) (1 - d ))), L])]; 
    RuleR[d_ > 0 \[Implies] x1_ ⩽ x2_] := 
      Module[{U}, (((x1 - x2  ⩽ U (1 - d )))^U)];
RuleR[d_ > 0 \[Implies] x1_ < x2_] := 
        Module[{U}, (((x1 - x2  < (U + 1) (1 - d )))^U)];
RuleR[
          d_ > 0 \[Implies] x1_ == x2_] := {RuleR[
            d > 0 \[Implies] x1 ⩾ x2], 
          RuleR[d > 0 \[Implies] x1 ⩽ x2]};

Function Lowerbound[A] computes the  lowerbound of  constraint A with  respects to the  given   Bounds, where  Bounds is specifed as  a list of terms of the form a≤x≤b.   
Lowerbound uses  auxiliary  function Lb.

Lowerbound[A_?AtomQ ] := Lb[A ];
Lowerbound[A_ ] :=  Map[Lb, A];
Lb[term : a_*  x_ ]  /;  a > 0  := 
        Module[{i = Position[
                  Bounds, _ ≤ 
                    x ≤ _][[1, 
                1]]}, 
          term /. {Bounds[[i, 
                  2]] -> 
                Bounds[[i, 
                  1]]}];
Lb[term : a_ * x_ ]  /;  a < 0   := 
        Module[{i = Position[
                  Bounds, _ ≤ 
                    x ≤ _][[1, 
                1]]}, 
          term /. {Bounds[[i, 
                  2]] -> 
                Bounds[[i, 
                  3]]}];
Lb[x_?VarQ ]   := 
      Bounds[[Position[
            Bounds, _ ≤ x ≤ _][[1, 
          1]], 1]]
Lb[a_ ]  := a

Function Upperbound[A] computes the  lowerbound of  constraint A with  respects to the  given   Bounds, where  Bounds is specifed as  a list of terms of the form a≤x≤b.   
Upperbound uses  auxiliary  function Lb.

Upperbound[A_] :=  Map[Ub, A]; 
Upperbound[A_?AtomQ] := Ub[A ];
Ub[term : a_*x_ ]  /;  a > 0  := 
        Module[{i = Position[
                  Bounds, _ ≤ 
                    x ≤ _][[1, 
                1]]}, 
          term /. {Bounds[[i, 
                  2]] -> 
                Bounds[[i, 
                  3]]}];
Ub[term : a_* x_ ]  /;  a < 0   := 
        Module[{i = Position[
                  Bounds, _ ≤ 
                    x ≤ _][[1, 
                1]]}, 
          term /. {Bounds[[i, 
                  2]] -> 
                Bounds[[i, 
                  1]]}];
Ub[x_?VarQ ]  := 
        Bounds[[Position[
              Bounds, _ ≤ 
                x ≤ _][[1, 
            1]], 3]]; 
Ub[a_ ]  :=  a;

Function RRC[x] (Remove Redundant Constraints) is defined below using the following    auxiliary functions:  
RCaux  checks whether a given constraint is redundant and outputs {} if redundant or else  a simplified constraint after substituting the    value of the Bounds.

RRC[A_] :=  Map[RCaux, A];
\(\(RCaux[\ \((A_ ≤ B_)\)\^U_\ ] := 
        Module[{Uw = Upperbound[A]}, 
		If[Uw > 0, 
            A ≤ \((B /. {U -> Uw})\), {}]];\)\)
\(\(RCaux[\(\((A_ < B_)\)\(\ \)\)\^U_] := 
	
        Module[{Uw = Upperbound[A]}, 
		If[Uw ≥ 0, 
            A < \((B /. {U -> Uw})\), {}]];\)\)
\(\(RCaux[\ \(\((A_ ≥ B_)\)\(\ \)\)\_L_]\  := 
        Module[{Lw = Lowerbound[A]}, 
		If[Lw < 0, 
            A ≥ \((B\  /. {L -> Lw})\), {}]];\)\)
\(\(RCaux[\(\((A_ > B_)\)\(\ \)\)\_L_] := 
	
        Module[{Lw = Lowerbound[A]}, 
		If[Lw ≤ 0, 
            A > \((B /. {L -> Lw})\), {}]];\)\)
RCaux[A_] := A;

Function MakeBounds[x] checks whether the input bound of each integer variable is right and   generates a decision variable and its bound for each  propositional    variable.

MakeBounds[ x_?BoundedQ ] :=  x;
MakeBounds[x_?VarQ] := 
        0 ≤ (Subscript[Pvar, x]) ≤ 1;

Founction PVarDecl[e] checks  whether each propositional variable is properly declared.

\(\(PVarDecl[v_] := 
        If[MemberQ[Bounds, v, {2, 3}], v, 
          Print["Propositional Variable ", \ \ v, " not declared."]; \ Throw[Bounds]];\)\)

Founction IPVarDecl[e] checks  whether each integer variable  is properly declared.

\(\(IPVarDecl[v_?VarQ] := 
        If[MemberQ[Bounds, v, 2], v, 
          Print["Integer variable ", \ \ v, " not declared."]; \ 
		Throw[Bounds]];\)\)
IPVarDecl[t : f_[__]] := Map[IPVarDecl, t];
IPVarDecl[x_Integer] := x;
IPVarDecl[x_Real] := x;
IPVarDecl[x_] :=  
      Module[{}, Print["Constraint ", x, " is not well formed"]; 
        Throw[Bounds]]

Founction IneqSimplify[e] simplifies expressions.

IneqSimplify[a_ >  b_]  :=  Simplify[a  - b]  > 0;
IneqSimplify[a_ ≥  b_]  :=  
        Simplify[a  - b]   ≥ 0;
IneqSimplify[a_ <  b_]  :=  Simplify[a  - b]  < 0;
IneqSimplify[a_ ≤  b_]  :=  
        Simplify[a  - b]   ≤ 0;

Founction Options[GenIP]  specifies that the generated IP-formulas will be simplified.

Options[GenIP] = {IPFormSimplify -> True};

Main function GenIP.  GenIP needs three arguments spec , decl and opts.  
spec is  a logical specification, 
decl is a list of propositional variables and  the bounds of  integer variables of the form  a ≤x≤b, and 
opts is an option to specify whether the generated IP-formulas will be simplified or not with IPFormSimplify->True  or IPFormSimplify->False.

\(GenIP[spec_, decl_, opts___] := \ 
      Catch[Block[{Pvar = δ\ , 
            Bounds = 
              Map[MakeBounds, decl]}\ , 	\ 
\ \ With[{ipform = 
                Flatten[{\(Composition[RRC, Flatten, RuleR, RuleF, RuleN, 
                        RuleT, RuleE2, RuleE1, RuleE4, RuleE3]\)[
                      spec]}]}, \ \ If[\(IPFormSimplify /. {opts}\) /. 
                  Options[GenIP], Map[IneqSimplify, ipform], ipform, 
                ipform] ⋃ Bounds]]]\)

Specification of nice

Let p be a boolean expression, then nice[p] gives p in "nice" form (i.e. " || " is replaced by "+", " && " is replaced by "·" and "! " is replaced by "\(TraditionalForm\`□\&_\)"):

nice[p_]:=p/.{And->Times,Or->Plus,Not->OverBar};

nice[(a || b) && (c || ! d) || ! a]

unnice[p_]:=p/.{Times->And,Plus->Or,OverBar->Not};

4. Computation of IP formulas

Example 1: Some Basic Constructions

Or

GenIP[p1 ∨ p2,{0 ≤ p1 ≤ 1, 
          0 ≤ p2 ≤ 1},IPFormSimplify -> False]

GenIP[p1 ∨ p2, {p1, p2}]

CNF[(a1||a2)&&(!a1||a2)]

CNF[(A⇒B)∧A]

And

GenIP[
      p1 ∧ p2, {0 ≤ p1 ≤ 1, 
        0 ≤ p2 ≤ 1}]

GenIP[p1 ∧ p2, {p1, p2}]

If then

GenIP[
      p1 ⇒ p2, {0 ≤ p1 ≤ 1, 
        0 ≤ p2 ≤ 1}]

GenIP[p1 ⇒ p2, {p1, p2}]

If and Only If

GenIP[
      p1 ⇔ p2, {0 ≤ p1 ≤ 1, 
        0 ≤ p2 ≤ 1}]

GenIP[p1 ⇔ p2, {p1, p2}]

Exclusive Or

eqns1 = 
      GenIP[(p1 ∨ 
              p2) ∧ (¬ (p1 ∧ p2)), {0 ≤ 
            p1 ≤ 1, 0 ≤ p2 ≤ 1}]

eqns1 = 
      GenIP[(p1 ∨ p2) ∧ (¬ (p1 ∧ p2)), {p1, 
          p2}]

Reduce[eqns1, {(Subscript[δ, p1]), (Subscript[δ, p2])}, Integers]

Meta predicate: 
 Let m(≥1) is an integer and S is a set of formulas
     -atleast (m, S) is a formula  
     -atmost (m, S) is a formula 
     -none (S) is a formula 

Additional Predicate:
     exactly(m,S)=atmost(m,S)atleast(m,S)

GenIP[
      CNF[atmost[3, {s1, s2, s3, s4, s5 }]], {s1, s2, s3, s4, 
        s5}]

GenIP[
      CNF[atleast[3, {s1, s2, s3, s4, s5 }]], {s1, s2, s3, s4, 
        s5}]

CNF[exactly[1,{q1,q2,q3}]∧exactly[1,{qq1,qq2,qq3}]∧((q1∧s1)⇒qq2)∧((q2∧s2)⇒qq3)∧((q3∧¬s2)⇒qq2)∧((q2∧¬s1)⇒qq1)∧((q1∧¬s1)⇒qq1)∧((q2∧¬s2)⇒qq2)∧((q2∧s1)⇒qq2)∧((q3∧s2)⇒qq3)]

GenIP[
      CNF[exactly[1, {q1, q2, q3}] ∧ 
          exactly[1, {qq1, qq2, 
              qq3}] ∧ ((q1 ∧ s1) ⇒ 
              qq2) ∧ ((q2 ∧ s2) ⇒ 
              qq3) ∧ ((q3 ∧ ¬ s2) ⇒ 
              qq2) ∧ ((q2 ∧ ¬ s1) ⇒ 
              qq1) ∧ ((q1 ∧ ¬ s1) ⇒ 
              qq1) ∧ ((q2 ∧ ¬ s2) ⇒ 
              qq2) ∧ ((q2 ∧ s1) ⇒ 
              qq2) ∧ ((q3 ∧ s2) ⇒ 
              qq3)], {s1, s2, q1, q2, q3, qq1, qq2, qq3, 
        0 ≤ q ≤ 2}]

Example 2: Logical Equivalence

⊕: exclusive or:  It can be proved that the xor (exclusive or) proposition can be converted to CNF : 
      p⊕q = (p∨q)∧(¬p∨¬q)
      (p3⇔(p1⊕p2)) =(p3⇒(p1⊕p2))∧((p1⊕p2)⇒p3)

Simplify[GenIP[p1⊕p2, {p1, p2}]]

Simplify[
      GenIP[(¬ p1 ∨ ¬ p2) ∧ (p1 ∨ p2), {p1, 
          p2}]]

GenIP[
      CNF[p3 ⇔ (p1⊕p2)], {p1, p2, 
        p3}]

GenIP[
      p3 ⇒ p1⊕p2, {p1, p2, p3}]

GenIP[¬ p3 ∨ (p1⊕p2), {p1, p2, p3}]

GenIP[(¬ p3 ∨ ¬ p1 ∨ ¬ p2) ∧ (¬ p3 ∨ p1 ∨ p2), {p1, p2, p3}]

GenIP[
      p1⊕p2 ⇒ p3, {p1, p2, p3}]

GenIP[(p1⊕p2) ⇒ p3, {p1, p2, 
        p3}]

GenIP[(¬ p1 ∨ ¬ p2) ∧ (p2 ∨ 
              p1) ⇒ p3, {p1, p2, p3}]

GenIP[(p1 ∧ p2) ∨ (¬ p2 ∧ ¬ p1) ∨ 
        p3, {p1, p2, p3}]

GenIP[
      CNF[(p1 ∧ p2) ∨ (¬ p2 ∧ ¬ p1) ∨ 
          p3], {p1, p2, p3}]

GenIP[(p1 ∨ ¬ p1 ∨ 
            p3) ∧ (p2 ∨ ¬ p1 ∨ 
            p3) ∧ (p1 ∨ ¬ p2 ∨ 
            p3) ∧ (p2 ∨ ¬ p2 ∨ p3), {p1, p2, 
        p3}]

It can be proved that the first proposition DNF can be converted to CNF : [Hooker, p47]
(¬p1∧p2)∨(p1∨¬p2): DNF of exclusive or
(¬p1∨¬p2)∧(p1∨p2): CNF or exclusive or
DNF:(¬p1∧p2)∨(p1∧¬p2)⟺(p1∨p2)∧(¬p1∨¬p2):CNF

GenIP[(¬ p1 ∧ 
            p2) ∨ (p1 ∨ ¬ p2), {p1, 
        p2}]

GenIP[(p1 ∨ 
            p2) ∧ (¬ p1 ∨ ¬ p2), {p1, 
        p2}]

Let write a boolean function which is  false when (p1,p2)=(1,1) or (0,0) and true otherwise:(¬p1∨¬p2)∧(p1∨p2)

GenIP[(¬ p1 ∨ ¬ p2) ∧ (p1 ∨ 
            p2), {p1, p2}]

GenIP[(p1 ∧ p2) ∨ (¬ p2 ∧ ¬ p1), {p1, 
        p2}]

Computational conversion from DNF to CNF:
DNF: e=(p1∧p2)∨(¬p2∧¬p1)

e = (p1 ∧ 
            p2) ∨ (¬ p2 ∧ ¬ p1)

GenIP[e, {p1, p2}]

CNF[e]

GenIP[CNF[e], {p1, p2}]

Convex Hull

<<Graphics`InequalityGraphics`

VA=GenIP[CNF[x3⇔(x1∧x2)],{ x1,x2,x3}]

InequalityPlot3D[ VA[[1]] ∧ VA[[2]] ∧ VA[[3]], {(Subscript[δ, x1]), 0, 1}, {(Subscript[δ, x2]), 0, 1}, {(Subscript[δ, x3]), 0, 1}]

VA1=GenIP[CNF[(x1∨x2)⇒x3],{ x1,x2,x3}]

InequalityPlot[ VA1[[1]] ∧ VA[[2]], {(Subscript[δ, x1]), 0, 1}, {(Subscript[δ, x2]), 0, 1}, {(Subscript[δ, x3]), 0, 1}]

GenIP[(p1 ⇒ p3), {p1, p3}]

GenIP[p3 ⇒ p1 ∨ p2, {p1, p2, p3}]

GenIP[
      p3 ⇒ (p1 ∨ p2), {p1, p2, p3}]

GenIP[(p2 ⇒ p3), {p2, p3}]

GenIP[(p1 ⇒ ¬ p2) ∧ (p2 ⇒ ¬ p1), {p1, p2}]

GenIP[
      CNF[p1 ⇒ 5  x - 2 ≤ 0], {p1, 
        0 ≤ x ≤ 3}]

GenIP[
      5  x ≤ 2 ⇒ p1, {p1, 
        0 ≤ x ≤ 1}]

GenIP[
      5  x ≤ 2 ⇔ p1, {p1, 
        0 ≤ x ≤ 1}]

GenIP[
      CNF[(p1 ∧ p2) ∨ (p3 ∧ p4)], {p1, p2, p3, 
        p4}]

CNF[(p1 ∧ p2) ∨ (p3 ∧ p4)]

GenIP[(p1 ∧ p2) ⇒ (p3 ∨ p4), {p1, 
        p2, p3, p4}]

GenIP[
      CNF[(p1 ∨ p2) ⇒ (p2 ∨ p4)], {p1, p2, 
        p3, p4}]

a = ¬ (p1 ∨ p2) ∨ (p2 ∨ p4)

CNF[a]

GenIP[CNF[a], {p1, p2, p3, p4}]

GenIP[CNF[¬(p1∨p2)∨((p1∨¬p2)∧¬p3)],{p1,p2,p3}]

Example 3: Solving IP Formulas

GenIP[((δ2) \[Implies] (δ1)) ∧ (¬ δ2 ∧ (f ≤ 
                0)), {0 ≤ δ1 ≤ 1, 
        0 ≤ δ2 ≤ 1, -1 ≤ 
          f ≤ 1}, IPFormSimplify -> False]

eqns = 
      GenIP[CNF[(y1 ⇔ 
                y2) ∧ (y2 \[Implies] (x ≥ 
                    0))], {0 ≤ y1 ≤ 1, 
          0 ≤ y2 ≤ 1, -10 ≤ 
            x ≤ 10}]

Reduce[eqns, {y1, y2, d$112}, Integers]

eqns = 
      GenIP[(y1 ⇔ (x ≥ 
                0)), {0 ≤ y1 ≤ 
            1, -10 ≤ x ≤ 10}]

GenIP[(p1 ⇔ (x ≥ 
              0)), {p1, -10 ≤ x ≤ 
          10}]

Reduce[eqns, {y1, y2, d$128, d$131}, Integers]

GenIP[(y1 ∨ y2 \[Implies] 
            y3 ∨ 
              y4) ∧ (¬ y1 ∧ (4  x1 + 3  x2 - 
                  x3 ⩾ 
                15)) ∧ (¬ y2 ∧ (5  x1 - 2  x2 + 
                  3  x3 ⩾ 
                15)) ∧ (¬ y3 ∧ (x1 + x2 + 
                  x3 ⩾ 
                10)) ∧ (¬ y4 ∧ (2  x1 + x2 + 
                  3  x3 ⩾ 15)), {1 ⩽ 
          x1 ≤ 5, 1 ⩽ x2 ≤ 5, 
        1 ⩽ x3 ≤ 5, 
        0 ⩽ y1 ≤ 1, 
        0 ⩽ y2 ≤ 1, 
        0 ⩽ y3 ≤ 1, 
        0 ⩽ y4 ≤ 1}]

GenIP[
      CNF[R2[(y1 ∨ y2 \[Implies] 
                y3 ∨ 
                  y4) ∧ (¬ y1 ∧ (4  x1 + 3  x2 - 
                      x3 ⩾ 
                    15)) ∧ (¬ y2 ∧ (5  x1 - 2  x2 + 
                      3  x3 ⩾ 
                    15)) ∧ (¬ y3 ∧ (x1 + x2 + 
                      x3 ⩾ 
                    10)) ∧ (¬ y4 ∧ (2  x1 + x2 + 
                      3  x3 ⩾ 
                    15))]], {1 ⩽ x1 ≤ 5, 
        1 ⩽ x2 ≤ 5, 
        1 ⩽ x3 ≤ 5, 
        0 ⩽ y1 ≤ 1, 
        0 ⩽ y2 ≤ 1, 
        0 ⩽ y3 ≤ 1, 
        0 ⩽ y4 ≤ 1}]

GenIP[
      CNF[(y1 ∨ y2 ⇔ y3 ∨ 
              y4) ∧ (¬ y1 ∧ (4  x1 + 3  x2 - 
                    x3 ⩾ 
                  15)) ∧ (¬ y2 ∧ (5  x1 - 2  x2 + 
                    3  x3 ⩾ 
                  15)) ∧ (¬ y3 ∧ (x1 + x2 + 
                    x3 ⩾ 
                  10)) ∧ (¬ y4 ∧ (2  x1 + x2 + 
                    3  x3 ⩾ 
                  15))], {1 ⩽ x1 ≤ 5, 
        1 ⩽ x2 ≤ 5, 
        1 ⩽ x3 ≤ 5, 
        0 ⩽ y1 ≤ 1, 
        0 ⩽ y2 ≤ 1, 
        0 ⩽ y3 ≤ 1, 
        0 ⩽ y4 ≤ 1}]

Example 4: Mixed Integer & Real Variables

GenIP[(q1⊕q2) ∧ ((q1 ∧ 
                p1) ⇒ 
            qq2) ∧ ((q1 ∧ ¬ p1) ⇒ 
            qq1) ∧ ((q2 ∧ p2) ⇒ 
            qq1) ∧ ((q2 ∧ ¬ p2) ⇒ 
            qq2), {p1, p2, q1, q2, qq1, qq2}]

GenIP[(p1 ⇔ 
            x ≥ 0) ∧ (p2 ⇔ 
            x ≥ 0), {p1, 
        p2, -5 ≤ x ≤ 10}]

GenIP[(q1⊕q2) ∧ ((q1 ∧ 
                p1) ⇒ 
            qq2) ∧ ((q1 ∧ ¬ p1) ⇒ 
            qq1) ∧ ((q2 ∧ p2) ⇒ 
            qq1) ∧ ((q2 ∧ ¬ p2) ⇒ 
            qq2) ∧ (p1 ⇔ 
            x ≥ 0) ∧ (p2 ⇔ 
            x < 0), {p1, p2, q1, q2, qq1, 
        qq2, -5 ≤ x ≤ 10}]

GenIP[(p1 ⇔ 
          x ≥ 0), {p1, -5 ≤ x ≤ 
          10}]

A1 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1) ∧ (¬ q1 ⇒ 
                z == 0), {q1, 
          0 ≤ x ≤ 2, -1 ≤ z ≤ 
            1}]

A1 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1) ∧ ((¬ q1) ⇒ 
              z == 0), {q1, 
          0 ≤ x ≤ 2, -1 ≤ z ≤ 
            1}]

A1 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1) ∨ ((¬ q1) ⇒ 
              z == 0), {q1, 
          0 ≤ x ≤ 2, -1 ≤ z ≤ 
            1}]

A1 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1)⊕(¬ q1 ⇒ 
                z == 0), {q1, 
          0 ≤ x ≤ 2, -1 ≤ z ≤ 
            1}]

A11 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1)⊕(q2 ⇒ z == 0), {q1, 
          q2, 0 ≤ x ≤ 2, -1 ≤ 
            z ≤ 1}]

A2 = 
      GenIP[(q1⊕q2) ∧ (q1 ⇒ 
              z == - x + 1) ∧ (q2 ⇒ 
              z == 0), {q1, q2, 
          0 ≤ x ≤ 10, -9 ≤ 
            z ≤ 1}]

Union[A1, A2]

Example 5: More Mixed Integer & Real Variables

GenIP[((x > 0) ⇒ 
            z == 
              2 x) ∧ ((¬ (x > 0)) ⇒ 
            z == x), {-1 ≤ x ≤ 
          1, -1 ≤ z ≤ 2}]

GenIP[((x > 0) ⇒ 
            z == 2 x) ∧ (((x ≤ 
                  0)) ⇒ 
            z == x), {-1 ≤ x ≤ 
          1, -1 ≤ z ≤ 2}]

GenIP[(((0 ≤ x) ∧ (x < 
                    3.14159/4)) ⇒ 
            z ==  .95791 x) ∧ (((3.14159/4 ≤ 
                    x) ∧ (x < 3.14159/2)) ⇒ 
            z == 0.45639 + 0.37681 x), {0 ≤ 
          x ≤ 3.14159, 
        0 ≤ z ≤ 2}]

GenIP[((x - y > 0) ⇒ 
            z == 
              2 x - 2 y) ∧ (((x - y < 
                  0)) ⇒ 
            z == (x - y)), {-1 ≤ x ≤ 
          1, -1 ≤ y ≤ 1, -2 ≤ 
          z ≤ 4}]

GenIP[(q1⊕q2) ∧ (qq1⊕qq2) ∧ ((q1 ∧ (x > 0)) ⇒ 
            qq2) ∧ ((q2 ∧ s) ⇒ 
            qq1), {q1, q2, qq1, qq2, 
        s, -2 ≤ x ≤ 2}]

5. More on IP Computation

Example 1: Transition Structures

Spec = (q1⊕q2) ∧ (q1 ∧ p1 \[Implies] 
              q2) ∧ (q1 ∧ ¬ p1 \[Implies] 
              q1) ∧ (q2 ∧ p2 \[Implies] 
              q1) ∧ (q2 ∧ ¬ p2 \[Implies] 
              q2);

eqns = GenIP[Spec, {q1, q2, p1, p2}]

Reduce[eqns, {(Subscript[δ, q1]), (Subscript[δ, q2])}, Integers]

Spec = 
        q1 ∧ (q1⊕q2) ∧ (q1 ∧ p1 \[Implies] 
              q2) ∧ (q1 ∧ ¬ p1 \[Implies] 
              q1) ∧ (q2 ∧ p2 \[Implies] 
              q1) ∧ (q2 ∧ ¬ p2 \[Implies] 
              q2);
eqns = GenIP[Spec, {q1, q2, p1, p2}]
Reduce[eqns, {(Subscript[δ, q1]), (Subscript[δ, q2])}, Integers]

Spec = (q1⊕q2) ∧ (q10 ∧ p1 \[Implies] 
              q2) ∧ (q10 ∧ ¬ p1 \[Implies] 
              q1) ∧ (q20 ∧ p2 \[Implies] 
              q1) ∧ (q20 ∧ ¬ p2 \[Implies] 
              q2);
eqns = 
      GenIP[Spec, {q10, q20, q1, q2, p1, p2}]
Reduce[eqns, {(Subscript[δ, q1]), (Subscript[δ, q2])}, Integers]

Spec = (q10⊕q20) ∧ (q1⊕q2) ∧ (q10 ∧ p1 \[Implies] 
              q2) ∧ (q10 ∧ ¬ p1 \[Implies] 
              q1) ∧ (q20 ∧ p2 \[Implies] 
              q1) ∧ (q20 ∧ ¬ p2 \[Implies] 
              q2);
eqns = 
      GenIP[Spec, {q10, q20, q1, q2, p1, p2}]
Reduce[eqns, {(Subscript[δ, q1]), (Subscript[δ, q2])}, Integers]

Spec = (q1⊕q2) ∧ (q10 ∧ s \[Implies] 
              q2) ∧ (q10 ∧ ¬ s \[Implies] 
              q1) ∧ (q20 ∧ ¬ s \[Implies] 
              q1) ∧ (q20 ∧ s \[Implies] q2);
eqns = GenIP[Spec, {q10, q20, q1, q2, s}]

Spec = (q1⊕q2) ∧ (q1 ∧ s \[Implies] 
              q2) ∧ (q1 ∧ ¬ s \[Implies] 
              q1) ∧ (q2 ∧ ¬ s \[Implies] 
              q1) ∧ (q2 ∧ s \[Implies] q2);
eqns = GenIP[Spec, {q1, q2, s}]

Spec = (q10⊕q20) ∧ (q1⊕q2) ∧ (q10 ∧ s \[Implies] 
              q2) ∧ (q10 ∧ ¬ s \[Implies] 
              q1) ∧ (q20 ∧ ¬ s \[Implies] 
              q1) ∧ (q20 ∧ s \[Implies] q2);
eqns = GenIP[Spec, {q10, q20, q1, q2, s}]

Spec = (q10⊕q20) ∧ (q1⊕q2) ∧ (q10 ∧ s \[Implies] 
              q2) ∧ (q10 ∧ (¬ s) \[Implies] 
              q1) ∧ (q20 ∧ (¬ s) \[Implies] 
              q1) ∧ (q20 ∧ s \[Implies] q2);
eqns = GenIP[Spec, {q10, q20, q1, q2, s}]

Spec = (q10⊕q20) ∧ (q1⊕q2) ∧ (q10 ∧ s \[Implies] 
              q2) ∧ (q10 ∧ (¬ s) \[Implies] 
              q1) ∧ (q20 ∧ s \[Implies] 
              q1) ∧ (q20 ∧ (¬ s) \[Implies] 
              q2);
eqns = GenIP[Spec, {q10, q20, q1, q2, s}]

Spec = (q1⊕q2) ∧ (q10 ∧ p1 \[Implies] 
              q2) ∧ (q10 ∧ ¬ p1 \[Implies] 
              q1) ∧ (q20 ∧ p2 \[Implies] 
              q1) ∧ (q20 ∧ ¬ p2 \[Implies] 
              q2) ∧ (p1 ⇔ (x ≥ 
                  0));

eqns = 
      GenIP[Spec, {q10, q20, q1, q2, p1, 
          p2, -1 ⩽ x ⩽ 1}]

Spec = (q1⊕q2) ∧ (q1 ∧ (x ⩽ 0) \[Implies] 
              q2) ∧ (q1 ∧ ¬ (x ⩽ 
                      0) \[Implies] 
              q1) ∧ (q2 ∧ (x > 0) \[Implies] 
              q1) ∧ (q2 ∧ ¬ (x > 0) \[Implies] 
              q2);

eqns = 
      GenIP[Spec, {q1, 
          q2, -1 ⩽ x ⩽ 1}]

GenIP[(q1 \[Implies] 
            z == 2 x1 - x2) ∧ (¬ q1 \[Implies] 
            z == 0), {q1, -1 ⩽ 
          x1 ⩽ 1, -2 ⩽ 
          x2 ⩽ 1, -2 ⩽ 
          z ⩽ 5}]

GenIP[(q1 \[Implies] 
            z == 2 x1 - x2) ∧ (¬ q1 \[Implies] 
            z == 0), {q1, -1 ⩽ 
          x1 ⩽ 1, 
        0 ⩽ x2 ⩽ 1, -2 ⩽ 
          z ⩽ 5}]

Example 2: More Transition Structures

A3=exactly[1,{q1,q2,q3}]∧exactly[1,{qq1,qq2,qq3}]∧((q1∧s1)⇒qq2)∧((q1∧p)⇒qq3)∧((q1∧¬(s1∨p))⇒qq1)∧((q2∧s2)⇒qq1)∧((q2∧¬s2)⇒qq2)∧((q3∧s3)⇒qq2)∧((q3∧¬s3)⇒qq3);

B1=GenIP[A3,{s1,s2,s3,p,q1,q2,q3,qq1,qq2,qq3}];

B1 // MatrixForm

A4 = 
        exactly[1, {q1, q2, q3}] ∧ 
          exactly[1, {qq1, qq2, 
              qq3}] ∧ ((q1 ∧ s1) ⇒ 
              qq2) ∧ ((q1 ∧ p) ⇒ 
              qq3) ∧ ((q1 ∧ ¬ (s1 ∨ 
                        p)) ⇒ 
              qq1) ∧ ((q2 ∧ s2) ⇒ 
              qq1) ∧ ((q2 ∧ ¬ s2) ⇒ 
              qq2) ∧ ((q3 ∧ s3) ⇒ 
              qq2) ∧ ((q3 ∧ ¬ s3) ⇒ 
              qq3) ∧ (p ⇔ (x > 
                  1));

B2=GenIP[A4,{s1,s2,s3,p,q1,q2,q3,qq1,qq2,qq3,-2≤x≤2 }];

CC = Intersection[B1, B2]

DD = Complement[B2, CC]

A5=exactly[1,{q1,q2,q3}]∧exactly[1,{qq1,qq2,qq3}]∧((q1∧s1)⇒qq2)∧((q1∧(x>1))⇒qq3)∧((q1∧¬(s1∨(x>1)))⇒qq1)∧((q2∧s2)⇒qq1)∧((q2∧¬s2)⇒qq2)∧((q3∧s3)⇒qq2)∧((q3∧¬s3)⇒qq3);

B3=GenIP[A5,{s1,s2,s3,q1,q2,q3,qq1,qq2,qq3,-2≤x≤2}];

B3 // MatrixForm

CC = Intersection[B1, B3]

Complement[B1, CC]

Complement[B3, CC]

A6=exactly[1,{q1,q2,q3}]∧exactly[1,{qq1,qq2,qq3}]∧((q1∧s)⇒qq2)∧((q1∧(i≤0))⇒qq3)∧((q1∧¬(s∨(i≤0)))⇒qq1)∧((q2∧(¬s∧(i>0)))⇒qq1)∧((q2∧(¬s∧(i>0)))⇒qq2)∧((q2∧¬((¬s∧(i>0))∨(¬s∧(i≤0))))⇒qq2)∧((q3∧s)⇒qq2)∧((q3∧(q≤1))⇒qq1)∧((q3∧¬(s∨(q≤1)))⇒qq3);

B6=GenIP[A6,{s,q1,q2,q3,qq1,qq2,qq3,-1≤i≤1,0≤q≤2}];

Example 3: 'If Then Else' and Other Structures

GenIP[(q1 \[Implies] 
            z == 2 x1 - x2) ∧ (¬ q1 \[Implies] 
            z == 0), {q1, -1 ⩽ 
          x1 ⩽ 1, 
        0 ⩽ x2 ⩽ 1, -2 ⩽ 
          z ⩽ 5}]

GenIP[(q1 \[Implies] 
            z == 2 x1 - x2) ∨ (¬ q1 \[Implies] 
            z == 0), {q1, -1 ⩽ 
          x1 ⩽ 1, 
        0 ⩽ x2 ⩽ 1, -2 ⩽ 
          z ⩽ 5}]

GenIP[(q1 ⇒ 
            z ==  (46/59) x + 
                17/60) ∧ ((¬ q1) ⇒ 
            z == 0), {q1, 
        0 ≤ x ≤ 2, -1 ≤ z ≤ 
          1}]

A1 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1) ∧ ((¬ q1) ⇒ 
              z == 0), {q1, 
          0 ≤ x ≤ 2, -1 ≤ z ≤ 
            1}]

Reduce[A1, {(Subscript[δ, q1])}, Integers]

A1 = 
      GenIP[(q1 ⇒ 
              z == - x + 
                  1) ∨ ((¬ q1) ⇒ 
              z == 0), {q1, 
          0 ≤ x ≤ 2, -1 ≤ z ≤ 
            1}]

Reduce[A1, {(Subscript[δ, q1])}, Integers]

CNF[(q1 ∧ p1) ∨ (¬ q1 ∧ p2)]

CNF[(¬ q1 ∨ (z == 
                2 x1 - x2)) ∨ (q1 ∨ (z == 
                0))]

DNF[LogicalExpand[(q1 \[Implies] p1)]]

6. Integer Programming using IP formulas

Example1

\(We\ buy\ nine\ types\ of\ stocks\ numbered\ by\ 1\ to\ 9. \ If\ three\ or\ more\ type\ of\ stocks {1\ to\ 5} 
            are\ bought\ \ or\ less\ than\ four\ types\)
\(of\ stocks\ {3\ to\ 6, 8, 
              9}\ are\ bought\ then\ at\ most\ \ two\ \ types\ of\ stocks\ {6\ to\ 9}\ will\ be\ bought\ unless\ none\ of\ the\ stocks\ \ {5\ to\ 7}\ are\ bought . 
\(Question : 
                Which\ stocks\ can\ we\ buy\ to\ get\ as\ many\ types\ as\ possible . 
1 - Formulate\ the\ problem\ in\ the\ L - 
                  plus\ \ by\ using\ propositional\ variable\)\)
                            2 - Obtain the IP - 
            formulas by using the functin GenIP
                            \(3 - Send\ the\ IP - 
            formulas\ and\ an\ on\ objective\ function\ Max\ \(∑\+\(i = 1\)\%9 δ\_\(s\_i\)\)\)

GenIP[((atleast[3, {s1, s2, s3, s4, s5 }] ∨  
                atmost[3, {s3, s4, s5, s6, s8, 
                    s9}]) ∧ ¬ none[{s5, s6, s7}]) \[Implies] 
        atmost[2, {s6, s7, s8, s9}], {s1, s2, s3, s4, s5, s6, s7, s8, 
        s9}]

eq1 = -1 + d1 + d2 + d3 ≥ 0 && 
        1 - d2 - (Subscript[δ, s5]) ≥ 0 && 
        5 - 3 d3 - (Subscript[δ, s1]) - (Subscript[δ, s2]) - (Subscript[δ, s3]) - (Subscript[δ, s4]) - (Subscript[δ, s5]) ≥ 0 && 1 - d2 - (Subscript[δ, s6]) ≥ 0 && 
        1 - d2 - (Subscript[δ, s7]) ≥ 0 && 
        4 - 2 d1 - (Subscript[δ, s6]) - (Subscript[δ, s7]) - (Subscript[δ, s8]) - (Subscript[δ, s9]) ≥ 
          0 && -4 d3 + (Subscript[δ, s3]) + (Subscript[δ, s4]) + (Subscript[δ, s5]) + (Subscript[δ, s6]) + (Subscript[δ, s8]) + (Subscript[δ, s9]) ≥ 0 && 
        0 ≤ d1 ≤ 1 && 0 ≤ d2 ≤ 1 && 
        0 ≤ d3 ≤ 1 && 
        0 ≤ (Subscript[δ, s1]) ≤ 1 && 
        0 ≤ (Subscript[δ, s2]) ≤ 1 && 
        0 ≤ (Subscript[δ, s3]) ≤ 1 && 
        0 ≤ (Subscript[δ, s4]) ≤ 1 && 
        0 ≤ (Subscript[δ, s5]) ≤ 1 && 
        0 ≤ (Subscript[δ, s6]) ≤ 1 && 
        0 ≤ (Subscript[δ, s7]) ≤ 1 && 
        0 ≤ (Subscript[δ, s8]) ≤ 1 && 
        0 ≤ (Subscript[δ, s9]) ≤ 1

NMaximize[{(Subscript[δ, s1]) + (Subscript[δ, s2])  + (Subscript[δ, s3])  + (Subscript[δ, s4])  + (Subscript[δ, s5])  + (Subscript[δ, s6])  + (Subscript[δ, s7]) + (Subscript[δ, s8]) + (Subscript[δ, s9]), 
        eq1 && ((Subscript[δ, s1]) | (Subscript[δ, s2]) | (Subscript[δ, s3]) |  (Subscript[δ, s4]) | (Subscript[δ, s5]) | (Subscript[δ, s6]) | (Subscript[δ, s7]) | (Subscript[δ, s8]) | (Subscript[δ, s9]) | 
                d1 | d2 | d3) ∈ 
            Integers}, {(Subscript[δ, s1]), (Subscript[δ, s2]) , (Subscript[δ, s3]) , (Subscript[δ, s4]) , (Subscript[δ, s5]) , (Subscript[δ, s6]) , (Subscript[δ, s7]), (Subscript[δ, s8]), (Subscript[δ, s9]), d1, d2, d3}]

Example2

\(If\ there\ are\ at\ most\ 2\ analyst\ \ or\ at\ most\ 3  
          administrators\ in\ a\ research\ group\ for\ a\ project\ 

        then\ there\ must\ be\ at\ most\ 8\ programmers\ or\ at\ least\ 7\ engineers\ and\ vice\ versa . 
\ \ \((x1\  ≤ \ 2\  ∨ \ 
                  x2\  ≤ 
                    3)\) ⇔ \((x3\  ≤ \ 
                8\  ∨ \ x4\  ≥ \ 7)\)\)

GenIP[(x1 ≤ 2 ∨ 
            x2 ≤ 3) ⇔ (x3 ≤ 
              8 ∨ x4 ≥ 7), {1 ≤ 
          x1 ≤ 10, 1 ≤ x2 ≤ 10, 
        1 ≤ x3 ≤ 10, 
        1 ≤ x4 ≤ 10}]

Ctraint2 = -2 d6 + x1 > 0 && -3 d6 + x2 > 
          0 && -8 d9 + x3 > 0 && -1 + d4 + d5 + d6 ≥ 
          0 && -1 + d7 + d8 + d9 ≥ 
          0 && -1 - 6 d4 + x4 ≥ 
          0 && -11 + 4 d9 + x4 < 0 && -10 + 8 d8 + x1 ≤ 
          0 && -10 + 7 d7 + x2 ≤ 
          0 && -10 + 2 d5 + x3 ≤ 0 && 
        0 ≤ d4 ≤ 1 && 0 ≤ d5 ≤ 1 && 
        0 ≤ d6 ≤ 1 && 0 ≤ d7 ≤ 1 && 
        0 ≤ d8 ≤ 1 && 0 ≤ d9 ≤ 1 && 
        1 ≤ x1 ≤ 10 && 
        1 ≤ x2 ≤ 10 && 
        1 ≤ x3 ≤ 10 && 
        1 ≤ x4 ≤ 10

X := {x1, x2, x3, x4, d4, d5, d6, d7, d8, d9}
Y := (x1 | x2 | x3 | x4 | d4 | d5 | d6 | d7 | d8 | d9)

Solutions = 
      NMinimize[{x1 + x2 + x3 + x4, Ctraint2 && Y ∈ Integers}, 
        X]

Example3 : Computational logic: Testing the Validity of a deduction by IP model [7], p256

The premises of the argument are
                 x1⇒(x2∨x3)
               ¬x2⇒(x1∧x4) 
                 x4⇒(x2∨x3)
The conclusion is
                      x2≥1

A=CNF[(x1⇒(x2∨x3))∧((¬x2)⇒(x1∧x4))∧(x4⇒(x2∨x3))]

AG=GenIP[A,{0≤x1≤1,0≤x2≤1,0≤x3≤1,0≤x4≤1}]

Constraints=Apply[And,AG]  (* Joined equation *)

NMinimize[{x2, Constraints}, {x1, x2, x3, x4, d122}]

Since x2=0 the conclusion x2=1 doe not follow from the premises i.e smith was not necessarily the 
murderer since we could have the situation in which jones did not meet Smith 
last night but Jones was lying and the murder still took place after midnight.

Example4 : Multi-vehicle Cooperative Control [6]

Two  state attacker  state machine
The attacker has two discrete modes :  
              attack and inactive
\(When\ in\ attack\ mode, \ 
          it\ moves\ towrad\ the\ Defense\ Zone\ at\ constant\ velocity\ along\ a\ straight\ line\ path\)
\(The\ attacker, \ 
          initially\ in\ attack\ mode\ at\ the\ beginning\ of\ play, \ 
          transitions\ to\ Defense\ Zone\  . Once\ inactive, \ 
          the\ attacker\ does\ not\ move\ and\ remains\ inactive\ for\ the\ remainder\ of\ play\)

\(ak1\ is\ a\ discrete\ state\ at\ time\ k\ immdiately\ after\ the\ transition\)
Attack mode : ak = 1 
Inactive mode :  ak = 0
Guard :  p1 = 1  attacker in defense zone
                  p2 = 1  attacker is intercepted
Position of the attacker at time k (pk, qk)
Dynamics
pk1 = pk + vp*Ta*ak
qk1 = qk + vq*Ta*ak
\(where\ \((vp, 
              vq)\)\ is\ the\ constant\ velocity\ of\ the\ attacker\ at\ position\ \((pk, qk)\)\)
               Ta is the  sampling time

Logical specification
The attacker starts in the attack state
\(If\ it\ enters\ the\ defense\ zone\ or\ if\ it\ is\ intercepted\ by\ the\ defender\ then\ it\ transitions\ to\ inactive\ state\) 
and remains in that state
ak = 1 and p1 = 0 and p2 = 0 then ak1
ak = 0 or p1 = 1 or p2 = 1 then ak1 = 
                  0
Is equivalent to
 ak1 = 1 iff ak = 1 and p1 = 0 and p2 = 
                  0

CNF[(¬ ak1 ∨ (ak ∧ ¬ p1 ∧ 
                    p2)) ∧ (¬ (ak ∧ ¬ p1 ∧ 
                      p2) ∨ ak1)] // ColumnForm // 
      TraditionalForm

7. Hybrid System Examples

Example 6: Hybrid System Transition Specifications
A power conditioning device is of a type often used in a high performance drive( weapon turrets, satellite) to isolate a DC supply from large current demands even for long period of time.
Because resistance is very low, current is high for switch closed – so switch should be closed for short time.
When the switch is closed, the PCS goal is to re-supply capacitor charge (maintain voltage) while limiting current drawn from primary source.

Power Conditionning device



s: switch closed
¬s: switch open

A simple hybrid system is a deterministic hybrid automaton (DHA) portrayed graphically in Figure 4. This figure illustrates a two-mode (or two discrete state) system. The modes are labeled (Subscript[q, 1]),(Subscript[q, 2]). The symbols (Subscript[q, 1]),(Subscript[q, 2]) are considered propositional variables that take values True or False, so that  (Subscript[q, i])=True implies that the system is in mode i. The system can only be in one mode at a time so that the proposition (Subscript[q, 1])⊕(Subscript[q, 2]) is always True. When the system is in mode i, the continuous state evolves according to the equation \(\(x\_i\)\& . \)=(Subscript[f, i]) (x, u). The symbols s a denote propositional statement called guard that is either True or False. The transitions illustrated take place if the appropriate guard is true. Thus, if the system is in mode 1, and , s = True then a transition to mode 2 takes place.
We can write the describing equations in a form similar to the MLD structure . First define the Boolean variables  (Subscript[δ, (Subscript[q, 1])]),(Subscript[δ, (Subscript[q, 2])]),(Subscript[δ, s]) such that (Subscript[δ, α])=1 if the proposition α= True, and  (Subscript[δ, α])=0 otherwise.   such that  if the proposition , and  otherwise. Then we can write the dynamics in the form \(\(x\_i\)\& . \)=(Subscript[δ, (Subscript[q, 1])])(Subscript[f, 1]) (x, u)+(Subscript[δ, (Subscript[q, 2])])(Subscript[f, 2]) (x, u)	. The system evolution must also satisfy the logical requirements:
1.	The system is either in mode 1 or mode 2 but not both, i.e., (Subscript[q, 1]) (t)⊕(Subscript[q, 2]) (t) =True
2.	If the system is in mode 1 at time t, and ¬s = True then it is in mode 2 at time \(\(t\^+\)\)otherwise it remains in mode 1, i.e.
           (((Subscript[q, 1])(t)∧¬s )⇒\(\(q\_2\) \((\(t\^+\))\)\))∧(( (Subscript[q, 1])(t)∧s )⇒\(\(q\_1\) \((\(t\^+\))\)\))=True
3.	Similarly, if the system is in mode 2 at time t, and s =True then it is in mode 1 at time \(\(t\^+\)\) otherwise it remains in mode 2, 	i.e.,    (((Subscript[q, 2])(t)∧s )⇒\(\(q\_1\) \((\(t\^+\))\)\))∧(( (Subscript[q, 2])(t)∧¬s )⇒\(\(q\_2\) \((\(t\^+\))\)\))=True

			Transition Diagram
Transition Diagram


			Transition Specifications
			
((Subscript[q, 1]) (t)⊕(Subscript[q, 2]) (t))∧(\(\(q\_1\) \((\(t\^+\))\)\)⊕\(\(q\_2\) \((\(t\^+\))\)\))∧(((Subscript[q, 1])(t)∧¬s) ⇒\(\(q\_2\) \((\(t\^+\))\)\))∧(( (Subscript[q, 1])(t)∧s) ⇒\(\(q\_1\) \((\(t\^+\))\)\))∧ (((Subscript[q, 2])(t)∧s) ⇒\(\(q\_1\) \((\(t\^+\))\)\))∧(( (Subscript[q, 2])(t)∧¬s )⇒\(\(\(q\_2\) \((\(t\^+\))\)\(\ \)\)\))

Now, the specification ,  spec, can be converted into an equivalent set of inequalities involving the integer-valued variables using the following notations.

(Subscript[q, 1]) (t)⊕(Subscript[q, 2]) (t) =  (Subscript[q, 1])⊕(Subscript[q, 2])  =exactly[1, {q1, q2}] 
\(\(q\_1\) \((\(t\^+\))\)\)⊕\(\(q\_2\) \((\(t\^+\))\)\)=(Subscript[qq, 1])⊕(Subscript[qq, 2])  =exactly[1, {qq1, qq2}]

spec = 
        exactly[1, {q1, q2}] ∧ 
          exactly[1, {qq1, 
              qq2}] ∧ ((q1 ∧ ¬ s) \[Implies] 
              qq2) ∧ ((q1 ∧ s) \[Implies] 
              qq1) ∧ ((q2 ∧ s) \[Implies] 
              qq1) ∧ ((q2 ∧ ¬ s) \[Implies] 
              qq2);

eqns = GenIP[spec, {q1, q2, qq1, qq2, s}]

Example 7: More Transition Structures

A3=exactly[1,{q1,q2,q3}]∧exactly[1,{qq1,qq2,qq3}]∧((q1∧s1)⇒qq2)∧((q1∧p)⇒qq3)∧((q1∧¬(s1∨p))⇒qq1)∧((q2∧s2)⇒qq1)∧((q2∧¬s2)⇒qq2)∧((q3∧s3)⇒qq2)∧((q3∧¬s3)⇒qq3);

B1=GenIP[A3,{s1,s2,s3,p,q1,q2,q3,qq1,qq2,qq3}];

B1 // MatrixForm

A4 = 
        exactly[1, {q1, q2, q3}] ∧ 
          exactly[1, {qq1, qq2, 
              qq3}] ∧ ((q1 ∧ s1) ⇒ 
              qq2) ∧ ((q1 ∧ p) ⇒ 
              qq3) ∧ ((q1 ∧ ¬ (s1 ∨ 
                        p)) ⇒ 
              qq1) ∧ ((q2 ∧ s2) ⇒ 
              qq1) ∧ ((q2 ∧ ¬ s2) ⇒ 
              qq2) ∧ ((q3 ∧ s3) ⇒ 
              qq2) ∧ ((q3 ∧ ¬ s3) ⇒ 
              qq3) ∧ (p ⇔ (x > 
                  1));

B2=GenIP[A4,{s1,s2,s3,p,q1,q2,q3,qq1,qq2,qq3,-2≤x≤2 }];

CC = Intersection[B1, B2]

DD = Complement[B2, CC]

A5=exactly[1,{q1,q2,q3}]∧exactly[1,{qq1,qq2,qq3}]∧((q1∧s1)⇒qq2)∧((q1∧(x>1))⇒qq3)∧((q1∧¬(s1∨(x>1)))⇒qq1)∧((q2∧s2)⇒qq1)∧((q2∧¬s2)⇒qq2)∧((q3∧s3)⇒qq2)∧((q3∧¬s3)⇒qq3);

B3=GenIP[A5,{s1,s2,s3,q1,q2,q3,qq1,qq2,qq3,-2≤x≤2}];

B3 // MatrixForm

8. References

[1] Li, Q., Y. Guo, et al. (1999). Transformation of Logical Specification into IP-formulas. 3rd International Mathematica Symposium (IMS '99), Hagenburg, Austria, Computational Mechanics Publications, WIT Press.
[2] Li, Q., Y. Guo, et al. (2000). "Modelling Integer Programming with Logic: Language and Implementation." IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E83-A (8): 1673-1680.
[3] Hooker, J. (2000). Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction, Wiley-Interscience.
[4] Bemporad, A. and M. Morari (1999). "Control of Systems Integrating Logic, Dynamics, and Constraints." Automatica 35: 402-427.
[4] Tyler, M. L. and M. Morari (1999). "Propositional Logic in Control and Monitoring Problems." Automatica 35 (4): 565-582.
[5] Williams, H. P. (1993). Model Building in Mathematical Programming, John Wiley and Sons.


[6] Matthew G. Earl, Raffaello D'Andrea, Multi-vehicle Cooperative Control Using Integer Programming
[7] J. E. Beasley ." Advances in Linear and Integer programming", Oxford Science Publication, 1996